A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), x:A, v:B(x).
(<x,v>  fpf-vals(eq;P;f))  {x  dom(f) & P(x) & v = f(x)} 

latex

Definitions

t  T, x(s), x:A. B(x), x:AB(x), P  Q, false, False, A, , (x  l), b, Type, Prop, b, x:AB(x), P & Q, P  Q, Unit, left+right, true, <a,b>, {T}, SQType(T), let x = a in b(x), f(x), x  dom(f), fpf-vals(eq;P;f), a:A fp B(a), EqDecider(T), f(a), x. t(x), remove-repeats(eq;L), type List, s = t, deq-member(eq;x;L), s ~ t, S  T, S  T, {x:A| B(x) }, tl(l), n-m, if a<b c ; d fi, i<j, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), x.A(x), Y, ||as||, a<b, AB, , , nil, Void, A & B, P  Q, P  Q, Dec(P), car.cdr, filter(P;l), map(f;as), zip(as;bs), eqof(d), p  q, 1of(t), 2of(t), True

Lemmas

true wf, subtype rel self, assert of bor, or functionality wrt iff, deq property, pi2 wf, pi1 wf, guard wf, bor wf, eqof wf, list-subtype, subtype rel list, cons member, decidable assert, nil member, decidable false, false wf, fpf wf, deq wf, bool sq, member-remove-repeats, btrue wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bnot wf, not wf, assert wf, l member wf, deq-member wf, bool wf, bfalse wf, remove-repeats wf